perm filename EXAM[AP,DBL] blob
sn#064641 filedate 1973-10-29 generic text, type T, neo UTF8
(FILECREATED "23-SEP-73 23:44:12" EXAM)
(DEFINEQ
(**
[NLAMBDA ZZZ NIL])
(ADDASSERT
[LAMBDA (ASSERTION)
(SETQ ASSERTIONLIST (CONS ASSERTION ASSERTIONLIST])
(ADDFNS
[LAMBDA (FNS)
(COND
[(ATOM FNS)
(COND
((MEMB FNS EXAMFNS)
EXAMFNS)
(T (SETQ EXAMFNS (MERGE (LIST FNS)
EXAMFNS]
(T (for FN in FNS do (ADDFNS FN])
(ARGNAMEPACK
[LAMBDA (NEWARG) (* Workhorse of
AUXCALLARGLIST.)
(COND
[(EQ (CAR NEWARG)
(QUOTE ARG))
(PACK (LIST (QUOTE ARG)
(CADR NEWARG]
(T (LIST (CAR NEWARG)
(AUXPACK (CADR NEWARG])
(ASSERT
[LAMBDA (ASSERTION)
(SETQ ASSERTIONKEY (REVCDR ASSERTION))
[SETQ ASSERTIONLIST (FOR ASSERTION1 IN ASSERTIONLIST
JOIN (COND
((EQUAL (REVCDR ASSERTION1)
ASSERTIONKEY)
NIL)
(T (LIST ASSERTION1]
(ADDASSERT ASSERTION])
(ASSERTED
[LAMBDA (ASSERTION)
(MEMBER ASSERTION ASSERTIONLIST])
(AUXCALLARGLIST
[LAMBDA (NEWARGLIST)
(* This function just returns a prettified version
of newarglist suitable for actual insertion in a
call to an auxilliary function within the
synthesized code. It changes forms like
(ARG 2) to atoms like ARG2 in the proper places.)
(FOR NEWARG IN NEWARGLIST COLLECT (CDR NEWARG])
(AUXPACK
[LAMBDA (NEWARG) (* Workhorse of
AUXCALLARGLIST.)
(COND
[(EQ (CAR NEWARG)
(QUOTE ARG))
(PACK (LIST (QUOTE ARG)
(CADR NEWARG]
(T (LIST (CAR NEWARG)
(AUXPACK (CADR NEWARG])
(AVALUE
[LAMBDA (ASSERTKEY)
(AVALUE1 ASSERTKEY ASSERTIONLIST])
(AVALUE1
[LAMBDA (ASSERTKEY ASSERTLIST)
(COND
((NULL ASSERTLIST)
(FAIL))
[(EQUAL (REVCDR (CAR ASSERTLIST))
ASSERTKEY)
(CAR (LAST (CAR ASSERTLIST]
(T (AVALUE1 ASSERTKEY (CDR ASSERTLIST])
(BAKTRAKPT
[NLAMBDA (SETFORM EVALFORM RESETFORM)
(* Upon evaluation, SETFROM is first evaluated to
set up initial and then EVALFORM is evaluated under
these conditions. Upon failure, RESETFORM is
evaluated and then evaluation of EVALFORM is again
attempted. If evaluation of EVALFORM is ever
successful, its value is returned as the value of
BAKTRAKPT; BAKTRAKPT itself fails only if either
evalform or resetform fails.)
(PROG (TEMP)
(EVAL SETFORM)
LOOP(COND
((SETQ TEMP (TRY EVALFORM))
(RETURN (CAR TEMP)))
(T (EVAL RESETFORM)
(GO LOOP])
(BOTHCDR
[LAMBDA (LIST)
(CDR (REVCDR LIST])
(BREAKDOWNRECURARGS
[LAMBDA (SYNTHLIST)
(PROG [NEWSYNTHLIST (RECURCALL (AVALUE (LIST (QUOTE RECURCALL)
CODE]
(* Returns a modified list with each recursive
argument <ARG> broken own into, e.g.,
(CAR <ARG>) and (CDR (CDR <ARG>)).
(for the case where CDDR recursion has been
sasserted).)
(FOR SYNTHPAIR IN SYNTHLIST JOIN
(* We will replace all SYNTHPAIRs for which a
RECURCALL assertion has been made.)
(COND
((SETQ RECUR (SASSOC
SYNTHPAIR RECURCALL))
(SPLITUP SYNTHPAIR
(CDR RECUR)))
(T (LIST SYNTHPAIR])
(BRUTESYNTH
[LAMBDA (CODE SYNTHLIST)
(PROG (SYNTH)
(* Tries to synthesize CODE by brute force
(no recursion or creation of auxilliary functions)
and either returns such a synthesis ofails.
Called by SYNTHESIS.)
(RETURN
(COND
((NULL CODE)
NIL)
(T
(CHOICE
(COND
((SETQ SYNTH (CDR (SASSOC CODE SYNTHLIST)))
SYNTH)
(T (FAIL)))
ONFAILURE
(CONSSYNTH CODE SYNTHLIST)
ONFAILURE
(COND
((ATOM CODE)
(FAIL))
(T
(* We try to brute synthesize each element of CODE
separately and return a LIST synthesis)
(CONS (QUOTE LIST)
(for CODEL in CODE
collect (BRUTESYNTH
CODEL
(PRUNEARGS (FLATTEN CODEL)
SYNTHLIST])
(CHOICE
[NLAMBDA CHOICEFORM
(PROG (LIST)
(BAKTRAKPT (SETQ LIST (REMOVESYNTAX CHOICEFORM))
(EVAL (CAR LIST))
(COND
((CDR LIST)
(SETQ LIST (CDR LIST)))
(T (FAIL])
(CONSSYNTH
[LAMBDA (CODE SYNTHLIST)
(PROG (CARSYNTH CDRSYNTH)
(* If (CDR CODE) is already synthexized, and is on
SYNTHLIST, then we set as a subgoal the brute
synthesis of (CAR CODE). If this succeeds, we return
(to BRUTESYNTH) a CONS synthesis.
If either subgoal fails, CONSSYNTH fails.)
(COND
([NOT (SETQ CDRSYNTH (CDR (SASSOC (CDR CODE)
SYNTHLIST]
(FAIL)))
(SETQ CARSYNTH (BRUTESYNTH (CAR CODE)
(PRUNEARGS (FLATTEN (CAR CODE))
SYNTHLIST)))
(RETURN (LIST (QUOTE CONS)
CARSYNTH CDRSYNTH])
(CONSTANTS
[LAMBDA (CODE ARGALIST)
(PROG (CODEATOMS ARGATOMS)
(SETQ CODEATOMS (REDUNDELIM (FLATTEN CODE)))
[SETQ ARGATOMS (REDUNDELIM
(FLATTEN (MAPCAR ARGALIST (FUNCTION (LAMBDA (ARGPAIR)
(CAR ARGPAIR]
(FLATTEN (MAPCAR CODEATOMS (FUNCTION (LAMBDA (CODEATOM)
(COND
((MEMB CODEATOM ARGATOMS)
NIL)
(T CODEATOM])
(CONTEXTSPLIT
[LAMBDA (ASSERTIONLIST)
(CONTEXTSPLIT1 NIL ASSERTIONLIST])
(CONTEXTSPLIT1
[LAMBDA (LOCAL PAST)
(COND
((NULL PAST)
(LIST LOCAL))
((EQ (CAR PAST)
(QUOTE ***))
(CONS LOCAL PAST))
(T (CONTEXTSPLIT1 (APPEND LOCAL (LIST (CAR PAST)))
(CDR PAST])
(DELFN
[LAMBDA (FNNAME)
(SETQ EXAMFNS (REMOVE FNNAME EXAMFNS])
(DIFTEMPFN
[LAMBDA (ELFORM1 ELFORM2)
(COND
[(NULL ELFORM1)
(COND
((NULL ELFORM2)
NIL)
(T (QUOTE FAILATOM]
((NULL ELFORM2)
(QUOTE FAILATOM))
((EQUAL ELFORM1 ELFORM2)
ELFORM1)
((OR (ATOM ELFORM1)
(ATOM ELFORM2))
(COND
((AND (NUMBERP ELFORM1)
(NUMBERP ELFORM2))
(SETQ GENVA (GENSYM))
(PUT GENVA (QUOTE VARIABLE)
T)
[PUT GENVA (QUOTE TRANS)
(PROGN (SETQ DIFF (IDIFFERENCE ELFORM2 ELFORM1))
(COND
((EQ DIFF 1)
(QUOTE (ADD1 *LAST)))
((EQ DIFF -1)
(QUOTE (SUB1 *LAST)))
(T (LIST (QUOTE IPLUS)
(QUOTE *LAST)
DIFF]
GENVA)))
(T (DOUBLEMAPCAR ELFORM1 ELFORM2 (FUNCTION DIFTEMPFN])
(DIREC
[LAMBDA (CODE SYNTHLIST DISTELEMENTS)
(COND
((NULL CODE)
(QUOTE FRONTGUESS))
((NULL (CDR CODE))
(QUOTE FRONTGUESS))
([LESSP (SETQ L1 (LENGTH (INTERSECTION (FLATTEN (CAR CODE))
DISTELEMENTS)))
(SETQ L2 (LENGTH (INTERSECTION
(FLATTEN (CAR (LAST CODE)))
DISTELEMENTS]
(QUOTE BACK))
((GREATERP L1 L2)
(QUOTE FRONT))
(T (DIREC (BOTHCDR CODE)
SYNTHLIST DISTELEMENTS])
(DIRECTION
[LAMBDA (CODE SYNTHLIST)
(DIREC CODE SYNTHLIST (DIST.ELS SYNTHLIST])
(DIST.ELS
[LAMBDA (SYNTHLIST)
(* At present, returns a list of the cars of
nonatomic arguments on the SYNTHLIST)
(COND
((NULL SYNTHLIST)
NIL)
((ATOM (CAAR SYNTHLIST))
(DIST.ELS (CDR SYNTHLIST)))
(T (UNION (LIST (CAAAR SYNTHLIST))
(DIST.ELS (CDR SYNTHLIST])
(DOUBLEMAPCAR
[LAMBDA (LIST1 LIST2 FN)
(COND
((NULL LIST1)
NIL)
(T (CONS (APPLY FN (LIST (CAR LIST1)
(CAR LIST2)))
(DOUBLEMAPCAR (CDR LIST1)
(CDR LIST2)
FN])
(ELFORM
[LAMBDA (SYNTHESIS)
(* Converts a synthesis of the form
(CAR (CDR (ARG 2))) to an elform
(EL 2 (ARG 2)), although in the present version it
is used only trivially, since SYNTHLIST is now
containing only arguments, already in the form
(ARG 2). Called by FINDVA)
(COND
((EQ (CAR SYNTHESIS)
(QUOTE ARG))
SYNTHESIS)
((EQ (CAR SYNTHESIS)
(QUOTE CAR))
(ELFORM1 (CADR SYNTHESIS)
1))
(T (FAIL (QUOTE (2 FROM ELFORM])
(ELFORM1
[LAMBDA (SYNTHESIS NUM)
(COND
((EQ (CAR SYNTHESIS)
(QUOTE ARG))
(LIST (QUOTE EL)
NUM SYNTHESIS))
((EQ (CAR SYNTHESIS)
(QUOTE CDR))
(ELFORM1 (CADR SYNTHESIS)
(ADD1 NUM)))
(T (PRINT (QUOTE (NOT IN ELFORM])
(ELNUM
[LAMBDA (EL LIST)
(* For EL an element of LIST, returns the position
of EL in LIST. e.g.- ELNUM
(C (A B C D)) = 3.0)
(COND
((NULL LIST)
NIL)
((EQ EL (CAR LIST))
1)
(T (COND
((SETQ NUMB (ELNUM EL (CDR LIST)))
(ADD1 NUMB))
(T NIL])
(EXAMARGS
[LAMBDA (FOON) (* Returns the example
input argument list for
an example function
FOO<n>)
(SETQ MYDEF (GETD FOON))
(SETQ COM (CADDR MYDEF))
(SETQ EXAMARGUMENTS (COND
((EQ (CADDDR COM)
(QUOTE TO))
(LIST (CADDR COM)))
[(EQ (CADR (CDDDDR COM))
(QUOTE TO))
(LIST (CADDR COM)
(CAR (CDDDDR COM]
(T (PRINT (QUOTE (CAN'T FIND THEM])
(EXAMPLE
[LAMBDA NIL
(PROG (FNNAME EXAMPLEARGS CODE ARGNUMBER DEFLIST)
(SETQ ASSERTIONLIST NIL)
(SETQ DEFLIST NIL)
(SETQ GENARGNUMBER 0)
(SETQQ YESRESPONSELIST (YES Y OK GO))
(PRINT (QUOTE (What shall I call the top-level function?)))
(SETQ FNNAME (READ))
(PRINT (QUOTE (OK. Now type in an example argument list.)))
(SETQ EXAMPLEARGS (READ))
(PRINT (QUOTE (And what would be the value of the function
with this argument list as input?)))
(SETQ CODE (READ))
(PRINT (QUOTE (OK, I'll try.)))
(SETQ ARGNUMBER 0)
[SYNTHESIS FNNAME CODE
(FOR EXAMARG IN EXAMPLEARGS
COLLECT (PROGN
(* This PROGN returns argpairs of the form
(X ARG 1) (for example argument X).)
(SETQ ARGNUMBER (ADD1 ARGNUMBER))
(CONS EXAMARG
(LIST (QUOTE ARG)
ARGNUMBER]
(RETURN (COND
(DEFLIST (PRINT (QUOTE (Does this look right?)))
(PRETTYPRINT DEFLIST))
(T (QUOTE (SORRY, BUT I CAN'T HACK THAT ONE.])
(FAIL
[LAMBDA (MESSAGE)
(COND
(MESSAGE (PRINT MESSAGE)))
(RETFROM (QUOTE TRY)
NIL])
(FINALN
[LAMBDA (LIST N)
(CDR (LASTN LIST N])
(FINDHEADSYNTH
[LAMBDA (CODE SPLITCODE SYNTHLIST ARGALIST AUXNUMBER)
(PROG [(HEADCODEATOMS (REDUNDELIM (FLATTEN (CAR SPLITCODE]
(CHOICE
[ASSERT (LIST (QUOTE HEADSYN)
CODE
(CHOICE (BRUTESYNTH (CAR SPLITCODE)
(PRUNEARGS HEADCODEATOMS
SYNTHLIST))
ONFAILURE
(BRUTESYNTH (CAR SPLITCODE)
(PRUNEARGS HEADCODEATOMS
(
BREAKDOWNRECURARGS SYNTHLIST]
ONFAILURE
(CHOICE
[PROG [(NEWSYNTHLIST (NEWSYNTHLISTFN (PRUNEARGS
HEADCODEATOMS
SYNTHLIST]
(SETQ TOPFNFLAG NIL)
[DEFINE
(PRETTYARGS
(LIST
(LIST
(PACK (LIST FNNAME (QUOTE .AUX)
AUXNUMBER))
(LIST (QUOTE LAMBDA)
[FOR SYNTHPAIR IN NEWSYNTHLIST
JOIN
(COND
((EQ (CAR (CDR SYNTHPAIR))
(QUOTE QUOTE))
NIL)
(T (LIST (CDR SYNTHPAIR]
(RECURSYN (PACK (LIST FNNAME
(QUOTE .AUX)
AUXNUMBER))
(CAR SPLITCODE)
NEWSYNTHLIST
(REMOVECONSTANTS
NEWSYNTHLIST)
(ADD1 AUXNUMBER]
(SETQ DEFLIST (CONS (PACK (LIST FNNAME
(QUOTE .AUX)
AUXNUMBER))
DEFLIST))
(ASSERT (LIST (QUOTE HEADSYN)
CODE
(CONS (PACK (LIST FNNAME
(QUOTE .AUX)
AUXNUMBER))
(AUXCALLARGLIST
(REMOVECONSTANTS
(PRUNEARGS HEADCODEATOMS
SYNTHLIST]
ONFAILURE
(PROG [(NEWSYNTHLIST (NEWSYNTHLISTFN (PRUNEARGS
HEADCODEATOMS
(BREAKDOWNRECURARGS
SYNTHLIST]
(SETQ TOPFNFLAG NIL)
[DEFINE
(PRETTYARGS
(LIST
(LIST
(PACK (LIST FNNAME (QUOTE .AUX)
AUXNUMBER))
(LIST (QUOTE LAMBDA)
[FOR SYNTHPAIR IN NEWSYNTHLIST
JOIN
(COND
((EQ (CAR (CDR SYNTHPAIR))
(QUOTE QUOTE))
NIL)
(T (LIST (CDR SYNTHPAIR]
(RECURSYN (PACK (LIST FNNAME
(QUOTE .AUX)
AUXNUMBER))
(CAR SPLITCODE)
NEWSYNTHLIST
(REMOVECONSTANTS
NEWSYNTHLIST)
(ADD1 AUXNUMBER]
(SETQ DEFLIST (CONS (PACK (LIST FNNAME
(QUOTE .AUX)
AUXNUMBER))
DEFLIST))
(ASSERT
(LIST (QUOTE HEADSYN)
CODE
(CONS (PACK (LIST FNNAME (QUOTE .AUX)
AUXNUMBER))
(AUXCALLARGLIST
(REMOVECONSTANTS
(PRUNEARGS HEADCODEATOMS
(BREAKDOWNRECURARGS
SYNTHLIST])
(FINDRECURSION
[LAMBDA (CODE SPLITCODE SYNTHLIST ARGALIST)
(* This function analyzes the recursive structure of
the divided output and initiates as subgoals the
synthesis of the productive and recursive parts,
calling synthesis in the process.
Called by recursyn.)
(* HEADDISTERS is called to find the
head-distinguishing elements and hence the recursive
arguments, along with the calling form of those
recursive arguments.)
(HEADDISTERS CODE SPLITCODE ARGALIST)
(* We ask the user for confirmation of the value of
the recursive call if the current goal is still the
synthesis of the user-specified
(top-level) function.)
(COND
((OR (NULL TOPFNFLAG)
(PROGN
(* Since we are currently trying to define the
top-level function, and not one of its auxilliary
functions, we first verify the recursive synthesis
with the user before spending time trying to
synthesize the productive part.
PRETTYRECURCALL is set to something of the form
" FOO( Q (B C D) ) " for purposes of quesioning the
user.)
[SETQ PRETTYRECURCALL
(for RECURPAIR in (AVALUE (LIST (QUOTE RECURCALL)
CODE))
collect (EVAL (SUBST (KWOTE (CAAR RECURPAIR))
(QUOTE *ARG)
(CDR RECURPAIR]
(PRINT (LIST (QUOTE DOES)
FNNAME PRETTYRECURCALL (QUOTE =)
(CADR SPLITCODE)
(QUOTE ?)))
(* If the user has confirmed the recursive call,
this part of the OR statement is true, and an
assertion of the synthesis of the recursive part
will be made.)
(MEMB (READ)
YESRESPONSELIST)))
[SETQ RECURCALL (for RECURPAIR
in (AVALUE (LIST (QUOTE RECURCALL)
CODE))
collect (SUBST (CDAR RECURPAIR)
(QUOTE *ARG)
(CDR RECURPAIR]
(ASSERT (LIST (QUOTE RECURSYN)
CODE
(CONS FNNAME RECURCALL])
(FINDTERM
[LAMBDA (CODE REMAINING RECURCALLS)
(PROG (NEWREMAINING)
(COND
[(NULL REMAINING)
(GENTERMCONDS RECURCALLS (AVALUE (LIST (QUOTE RECURDEPTH)
CODE]
(T
(SELECTQ
(AVALUE (LIST (QUOTE JOINFN)
CODE))
[CONS (COND
((EQUAL (ONCETHRU (AVALUE (LIST (QUOTE HEADSYN)
CODE))
RECURCALLS)
(CAR REMAINING))
(FINDTERM CODE (CDR REMAINING)
(NEXTTAILS RECURCALLS)))
(T (FAIL]
(APPEND
(FINDTERM CODE
(SEGREMAINDER
(ONCETHRU (AVALUE (LIST (QUOTE HEADSYN)
CODE))
RECURCALLS)
REMAINING)
(NEXTTAILS RECURCALLS)))
(HELP (QUOTE (SELECTQ DEFAULT: JOINFN ASSERTED
TO BE))
(AVALUE (LIST (QUOTE JOINFN)
CODE])
(FINDTERMSYNTH
[LAMBDA (CODE SPLITCODE)
(ASSERT (LIST (QUOTE TERMSYN)
CODE
(FINDTERM CODE (CADR SPLITCODE)
(NEXTTAILS (AVALUE (LIST (QUOTE RECURCALL)
CODE])
(FINDVA
[LAMBDA (VAR SYNTHLIST)
(* Returns an elform description of VAR if VAR is
built from atoms which are top-level members of some
argument<s> on SYNTHLIST. Called from TEMPLATE.)
(PROG (ELNUMBER DESCRIP ELDESCRIP)
(COND
([SOME SYNTHLIST (FUNCTION (LAMBDA (SYNTHPAIR)
(SETQ ELDESCRIP (COND
((EQUAL VAR (CAR SYNTHPAIR))
(ELFORM (CDR SYNTHPAIR)))
([AND (SETQ ELNUMBER (ELNUM VAR
(CAR SYNTHPAIR)))
(SETQ DESCRIP (ELFORM (CDR SYNTHPAIR]
(LIST (QUOTE EL)
ELNUMBER DESCRIP))
(T NIL]
ELDESCRIP)
(T (FAIL (QUOTE (1 FINDVA])
(FIRSTN
[LAMBDA (LIST N)
(COND
((NULL LIST)
NIL)
((ZEROP N)
NIL)
(T (CONS (CAR LIST)
(FIRSTN (CDR LIST)
(SUB1 N])
(FLATTEN
[LAMBDA (LIST)
(COND
((NULL LIST)
NIL)
((ATOM LIST)
(LIST LIST))
(T (APPEND (FLATTEN (CAR LIST))
(FLATTEN (CDR LIST])
(FOO1.AUX
[LAMBDA (ARG2 ARG3)
(COND
((NULL ARG3)
NIL)
(T (CONS (LIST ARG2 (CAR ARG3))
(FOO1.AUX ARG2 (CDR ARG3])
(FORCE
[LAMBDA (CODE SYNTHLIST CYCLESIZE)
(* Called from RECURSYN, this function makes a
template from the first two cycles and forces
successive cycles of elements into this template.
Upon the first match-failure, the forced elements
become the first sublist of the value, while the
remaining elements are the second sublist.)
(MATCHDIVISION (FIRSTN CODE (ITIMES CYCLESIZE 2))
(NTH CODE (ADD1 (ITIMES CYCLESIZE 2)))
(TEMPLATE (FIRSTN CODE CYCLESIZE)
(FIRSTN (NTH CODE (ADD1 CYCLESIZE))
CYCLESIZE)
SYNTHLIST)
CYCLESIZE])
(FORCETEST
[LAMBDA (FOON)
(FORCE (OUTCODE FOON)
(MAKESYN FOON)
CYC])
(GENTERMCONDS
[LAMBDA (RECURCONDS RECURDEPTHS)
(* Returns a list of null-check termination
conditions which includes all checks based on
recursive depth as well as all based on dissallowing
continuation past the point given in the example.)
(COND
((NULL RECURCONDS)
NIL)
(T (APPEND (COND
[(NOT (ZEROP (CDAR RECURDEPTHS)))
(REVERSE (TERMSYN1 (CDAAR RECURCONDS)
(IMAX (LENGTH (CAAAR RECURCONDS)
)
(SUB1 (CDAR RECURDEPTHS]
(T NIL))
(GENTERMCONDS (CDR RECURCONDS)
(CDR RECURDEPTHS])
(HEADDISTERS
[LAMBDA (CODE SPLITCODE ARGLIST)
(ASSERT (LIST (QUOTE HEADDIST)
CODE NIL))
(ASSERT (LIST (QUOTE RECURCALL)
CODE NIL))
(ASSERT (LIST (QUOTE RECURDEPTH)
CODE NIL))
[for
ARGPAIR in ARGLIST
do
[COND
[[AND (LISTP (CAR ARGPAIR))
(MEMBER (CAAR ARGPAIR)
(FLATTEN (CAR SPLITCODE)))
(NOT (MEMBER (CAAR ARGPAIR)
(FLATTEN (CADR SPLITCODE]
(* In this case, ARGPAIR:1:1 propagateostulated
productive part but not to the part we assume is
recursive, so ARGPAIR:1:1 DISTINGUISHES the
productive part.)
[ASSERT (LIST (QUOTE HEADDIST)
CODE
(CONS (CAAR ARGPAIR)
(LIST (QUOTE CAR)
(CDR ARGPAIR]
(ASSERT
(LIST (QUOTE RECURCALL)
CODE
(APPEND (AVALUE (LIST (QUOTE RECURCALL)
CODE))
(LIST (CONS ARGPAIR
(RECURCALLFN
(CDAR ARGPAIR)
(LIST (QUOTE CDR)
(CDR ARGPAIR))
SPLITCODE]
(T
(ASSERT
(LIST (QUOTE RECURCALL)
CODE
(APPEND
(AVALUE (LIST (QUOTE RECURCALL)
CODE))
(LIST (CONS ARGPAIR
(COND
((EQ (CAR (CDR ARGPAIR))
(QUOTE ARG))
(QUOTE *ARG))
((EQ (CAR (CDR ARGPAIR))
(QUOTE QUOTE))
(CDR ARGPAIR))
(T (FAIL]
(ASSERT (LIST (QUOTE RECURDEPTH)
CODE
(APPEND (AVALUE (LIST (QUOTE RECURDEPTH)
CODE))
(LIST (CONS ARGPAIR (RECURDEPTHFN
(CAR ARGPAIR)
SPLITCODE]
(COND
((NOT (AVALUE (LIST (QUOTE HEADDIST)
CODE)))
(FAIL])
(IMAX
[LAMBDA (N1 N2)
(COND
((ILESSP N1 N2)
N2)
(T N1])
(MAKESYN
[LAMBDA (FOON)
(MAPCAR (EXAMARGS FOON)
(FUNCTION (LAMBDA (ARG)
(CONS ARG (QUOTE (ARG 9])
(MATCHDIVISION
[LAMBDA (HEADCODE TAILCODE TEMPLAT CYCLESIZE)
(* RETURNS A LIST WHOSE FIRST SYBLIST IS THE
PRODUCTIVE PART AND WHOSE SECOND SUBLIST IS
RECURSIVE PART. Called by FORCE with all the code
initially in TAILCODE)
(COND
[(NULL TAILCODE)
(LIST (FIRSTN HEADCODE CYCLESIZE)
(NTH HEADCODE (ADD1 CYCLESIZE]
((MATCHES (FIRSTN TAILCODE CYCLESIZE)
(FINALN HEADCODE CYCLESIZE)
TEMPLAT)
(MATCHDIVISION (APPEND HEADCODE (FIRSTN TAILCODE CYCLESIZE))
(NTH TAILCODE (ADD1 CYCLESIZE))
TEMPLAT CYCLESIZE))
(T (LIST HEADCODE TAILCODE])
(MATCHES
[LAMBDA (ELEMENT LASTELEMENT TEMPLAT)
(* Workhorse predicate of MATCHDIVISION.
True if ELEMENT and LASTELEMENT match according to
the conditions of TEMPLATE)
(COND
((NULL ELEMENT)
(EQUAL ELEMENT LASTELEMENT))
[(ATOM ELEMENT)
(COND
((NOT (GETP TEMPLAT (QUOTE VARIABLE)))
(* TEMPLAIS A CONSTANT,
SO THE ELEMENT MUST BE
EXACTLY THAT CONSTANT)
(EQUAL ELEMENT TEMPLAT))
(T
(* TEMPLAT IS A VARIABLE, SO THE TWO ELEMENTS MUST
BE AS SPECIFIED BY THE DIFFERENCE TEMPLATE OF
TEMPLAT)
(SATISFYRELATIONS (FINDVA ELEMENT SYNTHLIST)
(FINDVA LASTELEMENT SYNTHLIST)
(GETP TEMPLAT (QUOTE DIFTEMP]
(T (* WE TEST FOR A MATCH
COMPONENT-BY-COMPONENT)
(AND (MATCHES (CAR ELEMENT)
(CAR LASTELEMENT)
(CAR TEMPLAT))
(MATCHES (CDR ELEMENT)
(CDR LASTELEMENT)
(CDR TEMPLAT])
(NEWSYNTHLISTFN
[LAMBDA (ARGALIST)
(FOR ARGPAIR IN ARGALIST COLLECT (SETQ GENARGNUMBER (ADD1
GENARGNUMBER))
(CONS (CAR ARGPAIR)
(LIST (QUOTE ARG)
GENARGNUMBER])
(NEXTTAILS
[LAMBDA (RECURCALLS)
(FOR RECUR IN RECURCALLS
COLLECT (CONS (CONS (EVAL (SUBST (KWOTE (CAAR RECUR))
(QUOTE *ARG)
(CDR RECUR)))
(CDAR RECUR))
(CDR RECUR])
(NOFAIL
[NLAMBDA (FORM)
(CHOICE (EVAL FORM)
ONFAILURE NIL])
(ONCETHRU
[LAMBDA (HEADSYNTH RECURCALLS) (* Returns the value of
HEADSYNTH when evaluated
with the current
RECURCALLS bindings)
(PROG ((LITERALHEADSYNTH HEADSYNTH))
(FOR RECUR IN RECURCALLS DO (SETQ LITERALHEADSYNTH
(SUBST (KWOTE (CAAR RECUR))
(CDAR RECUR)
LITERALHEADSYNTH)))
(RETURN (COND
((EVAL LITERALHEADSYNTH))
(T (FAIL])
(OUTCODE
[LAMBDA (FOON) (* Returns the example
output for an example
function FOO<n>)
(SETQ MYDEF (GETD FOON))
(SETQ COM (CADDR MYDEF))
(SETQ OUTCOD (COND
((EQ (CADDDR COM)
(QUOTE TO))
(CAR (CDDDDR COM)))
((EQ (CADR (CDDDDR COM))
(QUOTE TO))
(CADDR (CDDDDR COM)))
(T (PRINT (QUOTE (CAN'T FIND IT])
(POPASSERTIONLIST
[LAMBDA NIL
(COND
((NULL ASSERTIONLIST)
NIL)
((EQ (CAR ASSERTIONLIST)
(QUOTE ***))
(SETQ ASSERTIONLIST (CDR ASSERTIONLIST)))
(T (SETQ ASSERTIONLIST (CDR ASSERTIONLIST))
(POPASSERTIONLIST])
(PRETTYARGS
[LAMBDA (CALL)
(COND
((ATOM CALL)
CALL)
((EQ (CAR CALL)
(QUOTE ARG))
(ARGNAMEPACK CALL))
(T (FOR EL IN CALL COLLECT (PRETTYARGS EL])
(PRUNEARGS
[LAMBDA (CODEATOMS SYNTHLIST)
(* Returns a pruned SYNTHLIST, with all synthpairs
whose atoms do not all propagate to codeatoms
(the list of atoms in the output code) removed.
This may be too tight a restriction for later
versions.)
(COND
((NULL SYNTHLIST)
NIL)
[[EVERY (FLATTEN (CAAR SYNTHLIST))
(FUNCTION (LAMBDA (ARGATOM)
(MEMB ARGATOM CODEATOMS]
(CONS (CAR SYNTHLIST)
(PRUNEARGS CODEATOMS (CDR SYNTHLIST]
(T (PRUNEARGS CODEATOMS (CDR SYNTHLIST])
(RECURCALLFN
[LAMBDA (ARGEXAM ARGFORM SPLITCODE)
(* Returns the recursive call using a dummy atom
*ARG in place of the argument form, as for example
(CDR (CDR (CAR *ARG))), (if, e.g., ARGFORM was
(CAR (ARG 1)) and it seems to exhibit CDDR
recursion.) Called from HEADDISTERS to make a
RECURCALL assertion which is used in FINDRECURSION.)
(COND
([OR (NULL ARGEXAM)
(MEMB (CAR ARGEXAM)
(FLATTEN (CADR SPLITCODE]
(QUOTE (CDR *ARG)))
(T (RECURCALLFN (CDR ARGEXAM)
(LIST (QUOTE CDR)
ARGFORM)
SPLITCODE])
(RECURDEPTHFN
[LAMBDA (ARGEXAM SPLITCODE)
(* Returns recursive depth of ARGEXAM.
For example, if the first TWO elements of ARGEXAM
fail to propagate to the recursive output, the value
is 2)
(COND
([OR (ATOM ARGEXAM)
(MEMB (CAR ARGEXAM)
(FLATTEN (CADR SPLITCODE]
0)
(T (ADD1 (RECURDEPTHFN (CDR ARGEXAM)
SPLITCODE])
(RECURSYN
[LAMBDA (FNNAME CODE SYNTHLIST ARGALIST AUXNUMBER)
(PROG (SPLITCODE (CYCLESIZE 1)
(DIRECTION (DIRECTION CODE SYNTHLIST)))
(* Called from SYNTHESIS (to synthesize the
top-level function) or from FINDHEADSYNTH
(to synthesize the head of the function or one of
its auxilliaries), RECURSYN returns a complete
synthesis, ready to be inserted in a
lambda-definition. Auxilliary function definition is
also initiated.)
(BAKTRAKPT
(PROGN
(* This is the setup part of this BAKTRAKPT
expression, the form which is evaluated before the
first execution of the PROGN form which follows.)
(ASSERT (LIST (QUOTE CYCLESIZE)
CODE 1))
(ASSERT (LIST (QUOTE DIRECTION)
CODE DIRECTION)))
[PROGN
(* Find direction to read code, make a template, and
push it as far forward as possible, leaving the
produced part as the car of SPLITCODE, the tail as
the cdr.)
[SETQ SPLITCODE
(COND
[(ASSERTED (LIST (QUOTE DIRECTION)
CODE
(QUOTE BACK)))
(FORCE (REVERSE CODE)
SYNTHLIST
(AVALUE (LIST (QUOTE CYCLESIZE)
CODE]
(T (FORCE CODE SYNTHLIST (AVALUE (LIST (QUOTE
CYCLESIZE)
CODE]
(FINDRECURSION CODE SPLITCODE SYNTHLIST ARGALIST)
(FINDHEADSYNTH CODE SPLITCODE SYNTHLIST ARGALIST
AUXNUMBER)
(* We have now found the recursive structure of the
code, making all related assertions and satisfying
the subgoals of synthesizing the head and recursive
parts.)
[COND
[(OR (MEMBER (AVALUE (LIST (QUOTE DIRECTION)
CODE))
(QUOTE (BACK BACKGUESS)))
(IGREATERP (LENGTH (CAR SPLITCODE))
1))
(ASSERT (LIST (QUOTE JOINFN)
CODE
(QUOTE APPEND]
(T (ASSERT (LIST (QUOTE JOINFN)
CODE
(QUOTE CONS)))
(ASSERT (LIST (QUOTE HEADSYN)
CODE
(CADR (AVALUE (LIST (QUOTE HEADSYN)
CODE]
(* The join function has
been determined to be
either CONS or APPEND.)
(* We now synthesize the
body of the CODE.)
(FINDTERMSYNTH CODE SPLITCODE)
[ASSERT
(LIST
(QUOTE BODYSYN)
CODE
(SELECTQ (AVALUE (LIST (QUOTE DIRECTION)
CODE))
[(FRONT FRONTGUESS)
(LIST (AVALUE (LIST (QUOTE JOINFN)
CODE))
(AVALUE (LIST (QUOTE HEADSYN)
CODE))
(AVALUE (LIST (QUOTE RECURSYN)
CODE]
[(BACK BACKGUESS)
(LIST (AVALUE (LIST (LIST (QUOTE JOINFN)
CODE)))
(AVALUE (LIST (QUOTE RECURSYN)
CODE))
(AVALUE (LIST (QUOTE HEADSYN)
CODE]
(HELP (QUOTE (DIRECTION IS ASSERTED
TO BE))
(AVALUE (LIST DIRECTION CODE]
(* NOW WE TRY TO
SYNTHESIZE THE
TERMINATING CONDITIONS)
(APPEND (LIST (QUOTE COND))
(AVALUE (LIST (QUOTE TERMSYN)
CODE))
(LIST (LIST (QUOTE T)
(AVALUE (LIST (QUOTE BODYSYN)
CODE]
(PROGN
(* This is the reset block of this BAKTRAKPT
expression, that form which is evaluated each time
the previous block fails, after which the previous
block is re-executed)
(COND
[(EQ DIRECTION (QUOTE FRONTGUESS))
(PRINT (QUOTE (CHANGE DIRECTION TO BACKGUESS)))
(SETQQ DIRECTION BACKGUESS)
(ASSERT (QUOTE (DIRECTION CODE ' BACKGUESS]
[(ILESSP CYCLESIZE (LENGTH CODE))
(SETQ CYCLESIZE (ADD1 CYCLESIZE))
(PRINT (LIST (QUOTE INCREMENT)
(QUOTE CYCLESIZE)
(QUOTE TO)
CYCLESIZE))
(ASSERT (LIST (QUOTE CYCLESIZE)
CODE CYCLESIZE))
(COND
((EQ DIRECTION (QUOTE BACKGUESS))
(PRINT (QUOTE (AND CHANGE DIRECTION BACK
TO FRONTGUESS)))
(SETQQ DIRECTION FRONTGUESS)
(ASSERT (LIST (QUOTE DIRECTION)
CODE
(QUOTE FRONTGUESS]
(T (FAIL])
(REDUNDELIM
[LAMBDA (LIST)
(INTERSECTION LIST LIST])
(REMOVECONSTANTS
[LAMBDA (SYNTHLIST)
(FOR SYNTHPAIR IN SYNTHLIST JOIN (COND
((EQ (CAR (CDR SYNTHPAIR))
(QUOTE QUOTE))
NIL)
(T (LIST SYNTHPAIR])
(REMOVESYNTAX
[LAMBDA (ATTEMPTFORM)
(COND
((NULL ATTEMPTFORM)
NIL)
((EQ (CAAR ATTEMPTFORM)
(QUOTE *))
(REMOVESYNTAX (CDR ATTEMPTFORM)))
((NULL (CDR ATTEMPTFORM))
(LIST (CAR ATTEMPTFORM)))
[(EQ (CAADR ATTEMPTFORM)
(QUOTE *))
(REMOVESYNTAX (CONS (CAR ATTEMPTFORM)
(CDDR ATTEMPTFORM]
[(NEQ (CADR ATTEMPTFORM)
(QUOTE ONFAILURE))
(HELP (QUOTE (INCORRECT ATTEMPTLIST]
(T (CONS (CAR ATTEMPTFORM)
(REMOVESYNTAX (CDDR ATTEMPTFORM])
(REVCDR
[LAMBDA (LIST)
(COND
((ATOM LIST)
NIL)
((NULL (CDR LIST))
NIL)
(T (CONS (CAR LIST)
(REVCDR (CDR LIST])
(SATISFYRELATIONS
[LAMBDA (ELEMENTFORM LASTELEMENTFORM DIFTEMP)
(* A predicate called by MATCH which is true if the
two atoms in question, whose element forms are the
first two arguments, satisfy the conditions of the
difference descriptions associated with the atom
DIFTEMP.)
(COND
((NULL ELEMENTFORM)
(EQUAL ELEMENTFORM LASTELEMENTFORM))
[(ATOM ELEMENTFORM)
(COND
((NOT (GETP DIFTEMP (QUOTE VARIABLE)))
(* DIFTEMP IS A CONSTANT, AND MUST BE SOME LABEL
LIKE EL, ARG, ETC., WHICH IS THE SAME AS
ELEMENTFORM)
(EQUAL ELEMENTFORM DIFTEMP))
(T (* ELEMENTFORM AND
LASTELEMENTFORM MUST BE
NUMBERS SATISFYING THE
TRANS RELATION)
(AND (NUMBERP ELEMENTFORM)
(EQUAL ELEMENTFORM (EVAL (SUBST LASTELEMENTFORM
(QUOTE *LAST)
(GETP DIFTEMP
(QUOTE TRANS]
(T (AND (* WE TEST
ELEMENT-BY-ELEMENT)
(SATISFYRELATIONS (CAR ELEMENTFORM)
(CAR LASTELEMENTFORM)
(CAR DIFTEMP))
(SATISFYRELATIONS (CDR ELEMENTFORM)
(CDR LASTELEMENTFORM)
(CDR DIFTEMP])
(SEGREMAINDER
[LAMBDA (SEGMENT LIST)
(* If SEGMENT exactly matches some front segment of
LIST, returns the remaining tail of LIST.
Otherwise, fails)
(COND
((NULL SEGMENT)
LIST)
((EQUAL (CAR SEGMENT)
(CAR LIST))
(SEGREMAINDER (CDR SEGMENT)
(CDR LIST)))
(T (FAIL])
(SPLITUP
[LAMBDA (SYNTHPAIR RECURFORM)
(LIST (CONS (CAAR SYNTHPAIR)
(LIST (QUOTE CAR)
(CDR SYNTHPAIR)))
(CONS (EVAL (SUBST (KWOTE (CAR SYNTHPAIR))
(QUOTE *ARG)
RECURFORM))
(SUBST (CDR SYNTHPAIR)
(QUOTE *ARG)
RECURFORM])
(SYNTHESIS
[LAMBDA (FNNAME CODE ARGALIST)
(* This function sets synthlist to contain all
arguments on arglist plus all constants found in the
code, and then attempts to synthesize the code,
first by brute synthesis, then by a recursive
breakdown)
(SETQ TOPFNFLAG T)
[SETQ SYNTHLIST (PRUNEARGS
(FLATTEN CODE)
(APPEND ARGALIST (FOR CONSTANT IN (CONSTANTS CODE ARGALIST)
COLLECT (CONS CONSTANT (LIST (QUOTE QUOTE)
CONSTANT]
[DEFINE (PRETTYARGS (LIST (LIST FNNAME
(LIST (QUOTE LAMBDA)
(FOR ARG IN ARGALIST
COLLECT (CDR ARG))
(CHOICE (BRUTESYNTH CODE
SYNTHLIST)
(* We first try to define the top-level function by
brute force using the function BRUTESYNTH, which
returns as its value the synthesized code...)
ONFAILURE
(RECURSYN FNNAME CODE
SYNTHLIST
ARGALIST 1)
(* ...and if this fails, we call RECURSYN with
auxnumber 1 to indicate that the next auxilliary
function which is required, if any, should be named
FOO.AUX1)
]
(* F CHOICE P)
(SETQ DEFLIST (CONS FNNAME DEFLIST])
(TEMPLATE
[LAMBDA (FIRST SECOND SYNTHLIST)
(* Called by FORCE to return a template fitting the
elements FIRST and SECOND. This template in general
includes dummy "variable" atoms where exact matching
is not possible. Each variable atom has associated
descriptions of the two instances of this variable,
and may have as well an interpretable procedural
description of the difference between the instances,
which may be evaluated in, for example,
SATISFYRELATIONS to see if other pairs of variables
differ in the same ways.)
(COND
[(NULL FIRST)
(COND
((NULL SECOND)
NIL)
(T (FAIL]
((NULL SECOND)
(FAIL))
((EQUAL FIRST SECOND) FIRST)
((OR (ATOM FIRST)
(ATOM SECOND))
(SETQ GENVAR (GENSYM))
(PUT GENVAR (QUOTE VARIABLE)
T)
[PUT GENVAR (QUOTE DIFTEMP)
(DIFTEMPFN (PUT GENVAR (QUOTE INST1)
(FINDVA FIRST SYNTHLIST))
(PUT GENVAR (QUOTE INST2)
(FINDVA SECOND SYNTHLIST]
GENVAR)
(T (DOUBLEMAPCAR FIRST SECOND (FUNCTION (LAMBDA (EL1 EL2)
(TEMPLATE EL1 EL2 SYNTHLIST])
(TERMSYN
[LAMBDA (CODE SYNTHLIST)
(CONS (QUOTE COND)
(FOR DEPTHPAIR IN (AVALUE (LIST (QUOTE RECURDEPTH)
CODE))
JOIN (REVERSE (TERMSYN1 (CDAR DEPTHPAIR)
(CDR DEPTHPAIR])
(TERMSYN1
[LAMBDA (ARGFORM DEPTH)
(COND
((LESSP DEPTH 0)
NIL)
(T (CONS (LIST (LIST (QUOTE NULL)
(TERMSYN2 ARGFORM DEPTH))
(QUOTE NIL))
(TERMSYN1 ARGFORM (SUB1 DEPTH])
(TERMSYN2
[LAMBDA (ARGFORM DEPTH)
(COND
((EQ DEPTH 0)
ARGFORM)
(T (LIST (QUOTE CDR)
(TERMSYN2 ARGFORM (SUB1 DEPTH])
(TEST
[LAMBDA (EXAMPLEARGS CODE)
(SETQ ASSERTIONLIST NIL)
(SETQ DEFLIST NIL)
(SETQ GENARGNUMBER 0)
(SETQQ YESRESPONSELIST (YES Y OK GO))
(SETQ FNNAME (QUOTE FOO))
(SETQ ARGNUMBER 0)
[SYNTHESIS FNNAME CODE (FOR EXAMARG IN EXAMPLEARGS
COLLECT
(PROGN (SETQ ARGNUMBER (ADD1 ARGNUMBER))
(CONS EXAMARG
(LIST (QUOTE ARG)
ARGNUMBER]
(COND
(DEFLIST (PRINT (QUOTE (THIS LOOK RIGHT?)))
(PRETTYPRINT DEFLIST))
(T (QUOTE (SORRY, BUT I CAN'T HACK THAT ONE.])
(TRY
[LAMBDA (EVALFORM)
(LIST (EVAL EVALFORM])
)
(LISPXPRINT (QUOTE EXAMFNS)
T)
(RPAQQ EXAMFNS
(** ADDASSERT ADDFNS ARGNAMEPACK ASSERT ASSERTED
AUXCALLARGLIST AUXPACK AVALUE AVALUE1 BAKTRAKPT BOTHCDR
BREAKDOWNRECURARGS BRUTESYNTH CHOICE CONSSYNTH CONSTANTS
CONTEXTSPLIT CONTEXTSPLIT1 DELFN DIFTEMPFN DIREC DIRECTION
DIST.ELS DOUBLEMAPCAR ELFORM ELFORM1 ELNUM EXAMARGS
EXAMPLE FAIL FINALN FINDHEADSYNTH FINDRECURSION FINDTERM
FINDTERMSYNTH FINDVA FIRSTN FLATTEN FOO1.AUX FORCE
FORCETEST GENTERMCONDS HEADDISTERS IMAX MAKESYN
MATCHDIVISION MATCHES NEWSYNTHLISTFN NEXTTAILS NOFAIL
ONCETHRU OUTCODE POPASSERTIONLIST PRETTYARGS PRUNEARGS
RECURCALLFN RECURDEPTHFN RECURSYN REDUNDELIM
REMOVECONSTANTS REMOVESYNTAX REVCDR SATISFYRELATIONS
SEGREMAINDER SPLITUP SYNTHESIS TEMPLATE TERMSYN TERMSYN1
TERMSYN2 TEST TRY))
(LISPXPRINT (QUOTE EXAMVARS)
T)
(RPAQQ EXAMVARS (ASSERTIONLIST RECURCALLS))
(RPAQQ ASSERTIONLIST ([BODYSYN ((X A Y)
(X B Y)
(X C Y)
(X D Y))
(CONS (LIST (QUOTE X)
(CAR (ARG 1))
(QUOTE Y))
(FOO4 (CDR (ARG 1]
(TERMSYN ((X A Y)
(X B Y)
(X C Y)
(X D Y))
(((NULL (ARG 1))
NIL)))
(HEADSYN ((X A Y)
(X B Y)
(X C Y)
(X D Y))
(LIST (QUOTE X)
(CAR (ARG 1))
(QUOTE Y)))
(JOINFN ((X A Y)
(X B Y)
(X C Y)
(X D Y))
CONS)
[RECURSYN ((X A Y)
(X B Y)
(X C Y)
(X D Y))
(FOO4 (CDR (ARG 1]
[RECURDEPTH ((X A Y)
(X B Y)
(X C Y)
(X D Y))
((((A B C D)
ARG 1) . 1]
(RECURCALL ((X A Y)
(X B Y)
(X C Y)
(X D Y))
((((A B C D)
ARG 1)
CDR *ARG)))
(HEADDIST ((X A Y)
(X B Y)
(X C Y)
(X D Y))
(A CAR (ARG 1)))
(DIRECTION ((X A Y)
(X B Y)
(X C Y)
(X D Y))
FRONT)
(CYCLESIZE ((X A Y)
(X B Y)
(X C Y)
(X D Y))
1)))
(RPAQQ RECURCALLS ((((B C D)
ARG 1)
CDR *ARG)))
STOP